Nuprl Definition : es-height 11,40
es-height(es;e)
== if first(e)
== ifthen if isrcv(e) then es-height(es;sender(e))+1 else 0 fi 
== if isrcv(e)
== ifthen if es-height(es;sender(e)) <z es-height(es;pred(e))
== ifthen then es-height(es;pred(e))
== ifthen else es-height(es;sender(e))
== ifthen fi +1
== else es-height(es;pred(e))+1
== fi 

clarification:

es-height(es;e)
== if es-first(es; e)
== ifthen if es-isrcv(es; e) then es-height(es;es-sender(es; e))+1 else 0 fi 
== if es-isrcv(es; e)
== ifthen if es-height(es;es-sender(es; e)) <z es-height(es;es-pred(es; e))
== ifthen then es-height(es;es-pred(es; e))
== ifthen else es-height(es;es-sender(es; e))
== ifthen fi +1
== else es-height(es;es-pred(es; e))+1
== fi 
(recursive) 
latex

DefinitionsY, x.A(x), first(e), isrcv(e), if b then t else f fi , i <z j, sender(e), n+m, f(a), pred(e), #$n
FDL editor aliaseses-height

origin